$\forall$$A$, $B$, $C$:Type, ${\it +a}$:($A$$\rightarrow$$A$$\rightarrow$$A$), ${\it +b}$:($B$$\rightarrow$$B$$\rightarrow$$B$), ${\it +c}$:($C$$\rightarrow$$C$$\rightarrow$$C$), $f$:($A$$\rightarrow$$B$$\rightarrow$$C$). \\[0ex]IsBilinear($A$;$B$;$C$;${\it +a}$;${\it +b}$;${\it +c}$;$f$) $\in$ $\mathbb{P}$